Nuprl Lemma : ma-compatible_weakening 0,22
M1, M2:MsgA. M1 = M2  M1 || M2 
latex

DefinitionsP  Q, Prop, MsgA, M1 || M2, x:A. B(x), t  T
Lemmasma-compatible-self, ma-compatible wf, msga wf

origin